#pragma once
#include "GraphAlgorithms.h"
struct Lexem{
    int first_variable;
    int second_variable;
    bool is_first_true;
    bool is_second_true;
    Lexem(int first, int second, bool first_is_true, bool second_is_true) : first_variable(first), second_variable(second),
        is_first_true(first_is_true), is_second_true(second_is_true){}
        Lexem(){}
};
inline std::auto_ptr<Graph> MakeGraphFor2SAT(const std::vector<Lexem> expression, int variables_number){
    std::vector<edge> edges;
    int vertices_number = variables_number * 2;
    for(int lexem = 0; lexem < expression.size(); lexem++){
        int from,to;
        if(expression[lexem].is_first_true){
            from = expression[lexem].first_variable * 2 ;
        }
        else{
            from = expression[lexem].first_variable * 2 + 1;
        }
        if(!expression[lexem].is_second_true){
            to = expression[lexem].second_variable * 2;
        }
        else{
            to = expression[lexem].second_variable * 2 + 1;
        }
        edge new_edge(from,to);
        edges.push_back(new_edge);
        if(!expression[lexem].is_first_true){
            to = expression[lexem].first_variable * 2;
        } 
        else{
            to = expression[lexem].first_variable * 2 + 1;
        }
        if(expression[lexem].is_second_true){
            from = expression[lexem].second_variable * 2;
        }
        else{
            from = expression[lexem].second_variable * 2 + 1;
        }
        new_edge = edge(from,to);
        edges.push_back(new_edge);
    }
    return MakeCompactGraph(vertices_number, edges);
}


inline bool IfSolutionExists(std::vector<int> component_for_vertex){
    for(int vertex = 0; vertex < component_for_vertex.size(); vertex += 2){
        if(component_for_vertex[vertex] == component_for_vertex[vertex + 1]){
            return false;
        }
    }
    return true;
}

inline std::vector<bool> FindSolutionFor2SAT(int variables_number, std::vector<Lexem> expression){
    std::auto_ptr<Graph> graph = MakeGraphFor2SAT(expression, variables_number);
    TarjanAlgo tarjan(graph->GetNumberOfVertices());
    DepthFirstSearch(*graph, tarjan);
    std::vector<int> component_for_vertex = tarjan.GetComponentsForVertices();
    std::auto_ptr<Graph> condensation_graph = MakeGraphCondensation(*graph, tarjan.GetComponents());
    if(!IfSolutionExists(tarjan.GetComponentsForVertices())){
        std::vector<bool> answer(0);
        return answer;
    }
    std::vector<bool> answer(variables_number);
    TopologicalSort topological_sort(condensation_graph->GetNumberOfVertices());
    DepthFirstSearch(*condensation_graph, topological_sort);
    std::vector<int> sorted_order = topological_sort.GetSortedGraph();
    std::vector<bool> values_for_vertices(2 * variables_number, false);
    for(int component = 0; component < sorted_order.size(); component++){
        std::set<int> vertices_in_component = tarjan.GetComponents()[component];
        for(std::set<int>::iterator vertex = vertices_in_component.begin(); vertex != vertices_in_component.end(); vertex++){
            if (values_for_vertices[*vertex] == true) continue;
	    values_for_vertices[*vertex - *vertex%2 + (*vertex + 1)%2] = true;
	    answer[*vertex / 2] = *vertex % 2 ? true : false;
        }
    }
    return answer;
}


